There are two problems to be solved in the traditional System Theoretic Process Analysis (STPA) method. One is the lack of automation means of realization, the other is the ambiguity problem caused by natural language result analysis. To solve these problems, a software safety requirement analysis and verification method based on STPA was proposed. Firstly, the software safety requirements were extracted and converted into formal expressions by the algorithm. Secondly, the state diagram model was built to describe the logic of software safety control behaviors and converted the logic into the readable formal language. Finally, the formal verification was carried out by model checking technology. The effectiveness of the method was verified by the case of a weapon launch control system. The results show that the proposed method can generate the safety requirements automatically and perform formal verification to them, avoid the dependence on manual intervention and solve the natural language description problems in traditional methods.